YES 1.9040000000000001
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule List
| ((isSuffixOf :: (Eq a, Eq b) => [Either b a] -> [Either b a] -> Bool) :: (Eq b, Eq a) => [Either b a] -> [Either b a] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] _ | = | True |
isPrefixOf | _ [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
| isSuffixOf :: Eq a => [a] -> [a] -> Bool
isSuffixOf | x y | = | reverse x `isPrefixOf` reverse y |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((isSuffixOf :: (Eq a, Eq b) => [Either a b] -> [Either a b] -> Bool) :: (Eq a, Eq b) => [Either a b] -> [Either a b] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
| isSuffixOf :: Eq a => [a] -> [a] -> Bool
isSuffixOf | x y | = | reverse x `isPrefixOf` reverse y |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
| (isSuffixOf :: (Eq a, Eq b) => [Either a b] -> [Either a b] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
| isSuffixOf :: Eq a => [a] -> [a] -> Bool
isSuffixOf | x y | = | reverse x `isPrefixOf` reverse y |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xy5100), Succ(xy2600000)) → new_primPlusNat(xy5100, xy2600000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xy5100), Succ(xy2600000)) → new_primPlusNat(xy5100, xy2600000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xy23000), Succ(xy260000)) → new_primMulNat(xy23000, Succ(xy260000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xy23000), Succ(xy260000)) → new_primMulNat(xy23000, Succ(xy260000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xy2300), Succ(xy26000)) → new_primEqNat(xy2300, xy26000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xy2300), Succ(xy26000)) → new_primEqNat(xy2300, xy26000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs1(Just(xy230), Just(xy2600), app(app(app(ty_@3, gc), gd), ge)) → new_esEs(xy230, xy2600, gc, gd, ge)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(app(ty_@2, bdh), bea)) → new_esEs2(xy230, xy2600, bdh, bea)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(ty_[], da), cg) → new_esEs0(xy231, xy2601, da)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(ty_Maybe, bg)) → new_esEs1(xy232, xy2602, bg)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(app(ty_Either, ef), eg), bb, cg) → new_esEs3(xy230, xy2600, ef, eg)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(ty_[], bbb), bba) → new_esEs0(xy230, xy2600, bbb)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(ty_Maybe, baa)) → new_esEs1(xy231, xy2601, baa)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(app(ty_@2, bab), bac)) → new_esEs2(xy231, xy2601, bab, bac)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(ty_[], bf)) → new_esEs0(xy232, xy2602, bf)
new_esEs3(Left(xy230), Left(xy2600), app(ty_Maybe, bce), bcc) → new_esEs1(xy230, xy2600, bce)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(ty_Maybe, bbc), bba) → new_esEs1(xy230, xy2600, bbc)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(xy230, xy2600, beb, bec)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(app(ty_@2, bbd), bbe), bba) → new_esEs2(xy230, xy2600, bbd, bbe)
new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(app(app(ty_@3, fa), fb), fc)) → new_esEs(xy230, xy2600, fa, fb, fc)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(app(app(ty_@3, dg), dh), ea), bb, cg) → new_esEs(xy230, xy2600, dg, dh, ea)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(app(app(ty_@3, he), hf), hg)) → new_esEs(xy231, xy2601, he, hf, hg)
new_esEs1(Just(xy230), Just(xy2600), app(ty_[], gf)) → new_esEs0(xy230, xy2600, gf)
new_esEs3(Left(xy230), Left(xy2600), app(app(ty_Either, bch), bda), bcc) → new_esEs3(xy230, xy2600, bch, bda)
new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(app(ty_Either, ga), gb)) → new_esEs3(xy230, xy2600, ga, gb)
new_esEs1(Just(xy230), Just(xy2600), app(app(ty_Either, hb), hc)) → new_esEs3(xy230, xy2600, hb, hc)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(ty_Maybe, ec), bb, cg) → new_esEs1(xy230, xy2600, ec)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(ty_Maybe, db), cg) → new_esEs1(xy231, xy2601, db)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(app(ty_@2, ed), ee), bb, cg) → new_esEs2(xy230, xy2600, ed, ee)
new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(ty_Maybe, ff)) → new_esEs1(xy230, xy2600, ff)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs(xy230, xy2600, bdc, bdd, bde)
new_esEs3(Left(xy230), Left(xy2600), app(app(ty_@2, bcf), bcg), bcc) → new_esEs2(xy230, xy2600, bcf, bcg)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(app(app(ty_@3, baf), bag), bah), bba) → new_esEs(xy230, xy2600, baf, bag, bah)
new_esEs3(Left(xy230), Left(xy2600), app(ty_[], bcd), bcc) → new_esEs0(xy230, xy2600, bcd)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(app(ty_Either, bad), bae)) → new_esEs3(xy231, xy2601, bad, bae)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(app(ty_@2, dc), dd), cg) → new_esEs2(xy231, xy2601, dc, dd)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(ty_[], bdf)) → new_esEs0(xy230, xy2600, bdf)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(app(app(ty_@3, cd), ce), cf), cg) → new_esEs(xy231, xy2601, cd, ce, cf)
new_esEs3(Right(xy230), Right(xy2600), bdb, app(ty_Maybe, bdg)) → new_esEs1(xy230, xy2600, bdg)
new_esEs1(Just(xy230), Just(xy2600), app(ty_Maybe, gg)) → new_esEs1(xy230, xy2600, gg)
new_esEs1(Just(xy230), Just(xy2600), app(app(ty_@2, gh), ha)) → new_esEs2(xy230, xy2600, gh, ha)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(ty_[], eb), bb, cg) → new_esEs0(xy230, xy2600, eb)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(app(ty_@2, bh), ca)) → new_esEs2(xy232, xy2602, bh, ca)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(ty_[], hh)) → new_esEs0(xy231, xy2601, hh)
new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(ty_[], fd)) → new_esEs0(xy230, xy2600, fd)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(app(ty_Either, de), df), cg) → new_esEs3(xy231, xy2601, de, df)
new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(app(ty_Either, bbf), bbg), bba) → new_esEs3(xy230, xy2600, bbf, bbg)
new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(app(ty_@2, fg), fh)) → new_esEs2(xy230, xy2600, fg, fh)
new_esEs3(Left(xy230), Left(xy2600), app(app(app(ty_@3, bbh), bca), bcb), bcc) → new_esEs(xy230, xy2600, bbh, bca, bcb)
new_esEs0(:(xy230, xy231), :(xy2600, xy2601), eh) → new_esEs0(xy231, xy2601, eh)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(app(ty_Either, cb), cc)) → new_esEs3(xy232, xy2602, cb, cc)
new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(app(app(ty_@3, bc), bd), be)) → new_esEs(xy232, xy2602, bc, bd, be)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(ty_Maybe, ff)) → new_esEs1(xy230, xy2600, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(app(ty_Either, ga), gb)) → new_esEs3(xy230, xy2600, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(app(app(ty_@3, fa), fb), fc)) → new_esEs(xy230, xy2600, fa, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Just(xy230), Just(xy2600), app(ty_Maybe, gg)) → new_esEs1(xy230, xy2600, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Just(xy230), Just(xy2600), app(app(ty_Either, hb), hc)) → new_esEs3(xy230, xy2600, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Just(xy230), Just(xy2600), app(app(app(ty_@3, gc), gd), ge)) → new_esEs(xy230, xy2600, gc, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(app(ty_@2, fg), fh)) → new_esEs2(xy230, xy2600, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Just(xy230), Just(xy2600), app(app(ty_@2, gh), ha)) → new_esEs2(xy230, xy2600, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Just(xy230), Just(xy2600), app(ty_[], gf)) → new_esEs0(xy230, xy2600, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(ty_Maybe, bg)) → new_esEs1(xy232, xy2602, bg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(ty_Maybe, ec), bb, cg) → new_esEs1(xy230, xy2600, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(ty_Maybe, db), cg) → new_esEs1(xy231, xy2601, db)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(app(ty_Either, ef), eg), bb, cg) → new_esEs3(xy230, xy2600, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(app(ty_Either, de), df), cg) → new_esEs3(xy231, xy2601, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(app(ty_Either, cb), cc)) → new_esEs3(xy232, xy2602, cb, cc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(app(app(ty_@3, dg), dh), ea), bb, cg) → new_esEs(xy230, xy2600, dg, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(app(app(ty_@3, cd), ce), cf), cg) → new_esEs(xy231, xy2601, cd, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(app(app(ty_@3, bc), bd), be)) → new_esEs(xy232, xy2602, bc, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(app(ty_@2, ed), ee), bb, cg) → new_esEs2(xy230, xy2600, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(app(ty_@2, dc), dd), cg) → new_esEs2(xy231, xy2601, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(app(ty_@2, bh), ca)) → new_esEs2(xy232, xy2602, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, app(ty_[], da), cg) → new_esEs0(xy231, xy2601, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), ba, bb, app(ty_[], bf)) → new_esEs0(xy232, xy2602, bf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs(@3(xy230, xy231, xy232), @3(xy2600, xy2601, xy2602), app(ty_[], eb), bb, cg) → new_esEs0(xy230, xy2600, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(ty_Maybe, baa)) → new_esEs1(xy231, xy2601, baa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(ty_Maybe, bbc), bba) → new_esEs1(xy230, xy2600, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Left(xy230), Left(xy2600), app(ty_Maybe, bce), bcc) → new_esEs1(xy230, xy2600, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Right(xy230), Right(xy2600), bdb, app(ty_Maybe, bdg)) → new_esEs1(xy230, xy2600, bdg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(app(ty_Either, bad), bae)) → new_esEs3(xy231, xy2601, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(app(ty_Either, bbf), bbg), bba) → new_esEs3(xy230, xy2600, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(app(app(ty_@3, he), hf), hg)) → new_esEs(xy231, xy2601, he, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(app(app(ty_@3, baf), bag), bah), bba) → new_esEs(xy230, xy2600, baf, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(app(ty_@2, bab), bac)) → new_esEs2(xy231, xy2601, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(app(ty_@2, bbd), bbe), bba) → new_esEs2(xy230, xy2600, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), app(ty_[], bbb), bba) → new_esEs0(xy230, xy2600, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(xy230, xy231), @2(xy2600, xy2601), hd, app(ty_[], hh)) → new_esEs0(xy231, xy2601, hh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Right(xy230), Right(xy2600), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(xy230, xy2600, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Left(xy230), Left(xy2600), app(app(ty_Either, bch), bda), bcc) → new_esEs3(xy230, xy2600, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(xy230, xy231), :(xy2600, xy2601), app(ty_[], fd)) → new_esEs0(xy230, xy2600, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(xy230, xy231), :(xy2600, xy2601), eh) → new_esEs0(xy231, xy2601, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs3(Right(xy230), Right(xy2600), bdb, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs(xy230, xy2600, bdc, bdd, bde)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(Left(xy230), Left(xy2600), app(app(app(ty_@3, bbh), bca), bcb), bcc) → new_esEs(xy230, xy2600, bbh, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Right(xy230), Right(xy2600), bdb, app(app(ty_@2, bdh), bea)) → new_esEs2(xy230, xy2600, bdh, bea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Left(xy230), Left(xy2600), app(app(ty_@2, bcf), bcg), bcc) → new_esEs2(xy230, xy2600, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Left(xy230), Left(xy2600), app(ty_[], bcd), bcc) → new_esEs0(xy230, xy2600, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Right(xy230), Right(xy2600), bdb, app(ty_[], bdf)) → new_esEs0(xy230, xy2600, bdf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf(:(xy220, xy221), :(xy2610, xy2611), ba) → new_isPrefixOf(xy221, xy2611, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf(:(xy220, xy221), :(xy2610, xy2611), ba) → new_isPrefixOf(xy221, xy2611, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf0(xy23, xy22, xy26, :(xy2510, xy2511), ba) → new_isPrefixOf0(xy23, xy22, new_flip(xy26, xy2510, ba), xy2511, ba)
The TRS R consists of the following rules:
new_flip(xy22, xy23, ba) → :(xy23, xy22)
The set Q consists of the following terms:
new_flip(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf0(xy23, xy22, xy26, :(xy2510, xy2511), ba) → new_isPrefixOf0(xy23, xy22, new_flip(xy26, xy2510, ba), xy2511, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 4, 5 >= 5
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf1(xy22, xy23, :(xy240, xy241), xy25, ba) → new_isPrefixOf1(new_flip(xy22, xy23, ba), xy240, xy241, xy25, ba)
The TRS R consists of the following rules:
new_flip(xy22, xy23, ba) → :(xy23, xy22)
The set Q consists of the following terms:
new_flip(x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf1(xy22, xy23, :(xy240, xy241), xy25, ba) → new_isPrefixOf1(new_flip(xy22, xy23, ba), xy240, xy241, xy25, ba)
The graph contains the following edges 3 > 2, 3 > 3, 4 >= 4, 5 >= 5